ds:fpf(Id; x.Type), da:fpf(Knd; k.Type), es:event_system{i:l}, i:Id,
LL:(event-info(ds;da) List List), e1,e2:{e:es-E(es)| loc(e) = i} , L:(event-info(ds;da) List).
l_all(LL; (event-info(ds;da) List); L.((L = [])))
 ((L = []))
 (x:Id. subtype_rel(es-vartype(es; i; x); fpf-cap(ds; id-deq; x; top)))
 (e:es-E(es). 
 (loc(e) = i)  subtype_rel(es-valtype(es; e); fpf-cap(da; Kind-deq; es-kind(es; e); top)))
 (es-hist{i:l}(es;e1;e2) = append(concat(LL); L)  (event-info(ds;da) List))
 (f:int_seg(0; (||LL|| + 1)){e:es-E(es)| loc(e) = i} 
 ((((f(0) = e1)  es-le(es; (f(||LL||)); e2))
 (c (i:int_seg(0; ||LL||). es-locl(es; (f(i)); (f(i + 1))))
 (c ((i:int_seg(0; ||LL||). 
 (c es-hist{i:l}(es;f(i);es-pred(es; (f(i + 1)))) = LL[i]  (event-info(ds;da) List))
 (c  (es-hist{i:l}(es;f(||LL||);e2) = L)))) 

latex

Definitions

x:A. B(x), t  T, x. t(x), P  Q, A, append(as; bs), concat(ll), x:A. B(x), int_seg(i; j), ||as||, A c B, P  Q, es-le(es; e; e'), reduce(f; k; as), Y, lelt(i; j; k), A  B, prop{i:l}, P  Q, P  Q, P  Q, top, subtype(S; T), if b then t else f fi , tt, ff, (i = j), T, True, sq_type(T), guard(T), False, l[i], hd(l), nth_tl(n;as), i z j, b, i <z j, x(s), decidable(P), e(e1,e2].P(e), es-locl(es; e; e'), , Unit,

Lemmas

event-info wf, Id wf, event system wf, fpf wf, Knd wf, int seg wf, false wf, es-locl wf, es-hist wf, es-E wf, es-loc wf, es-valtype wf, fpf-cap wf, Kind-deq wf, es-kind wf, top wf, es-vartype wf, id-deq wf, not wf, l all wf, decidable es-locl, null-es-hist, es-le-not-locl, concat-cons, append assoc sq, concat wf, es-hist-is-append, append wf, l all cons, not functionality wrt iff, append is nil, es-le-loc, es-loc-pred, es-locl-iff, eq int wf, bool wf, iff transitivity, assert wf, eqtt to assert, assert of eq int, bnot wf, eqff to assert, assert of bnot, length wf1, non neg length, es-le wf, squash wf, true wf, le wf, es-first wf, es-pred wf, ifthenelse wf, select cons tl sq, length cons, select wf